健全性の定義 (Γ ⊢ φ ⇒ Γ ⊨ φ)

健全性Γ⊢φ⇒Γ⊨φは、形式体系で導出できる命題が、意味論上もすべてのモデルで成り立つことを表す。推論規則が誤った結論を作らないという保証である。

仕組みと確認

公理と各推論規則について、前提が真なら結論も真になることを示し、証明の長さに関する帰納法で全証明へ拡張する。モデルと解釈を明示する。

限界と注意点

健全性は完全性・決定可能性・仕様の正しさとは別である。健全でも必要な真理をすべて証明できず、モデル化や外部公理の誤りも防げない。